| 翻訳と辞書 |
| refinement calculus ： ウィキペディア英語版 |
refinement calculus
The refinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an efficiently executable program.
Proponents include Ralph-Johan Back, who originated the approach in his 1978 PhD thesis ''On the Correctness of Refinement Steps in Program Development'', and Carroll Morgan, especially with his book ''(Programming from Specifications )'' (Prentice Hall, 2nd edition, 1994, ISBN 0-13-123274-6). In the latter case, the motivation was to link Abrial's specification notation Z, via a rigorous relation of behaviour-preserving program refinement, to an executable programming notation based on Dijkstra's language of guarded commands. ''Behaviour-preserving'' in this case means that any Hoare triple satisfied by a program should also be satisfied by any refinement of it, which notion leads directly to ''(specification statements )'' as pre- and postconditions standing, on their own, for any program that could soundly be placed between them.
== External links ==
* (Refinement Calculus information )
* (Refinement Calculus tutorial )
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』
■ウィキペディアで「refinement calculus」の詳細全文を読む
スポンサード リンク
| 翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|